ePMC

Benchmark
Model:pnueli-zuck v.1 (MDP)
Parameter(s)N = 5
Property:live (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files pnueli-zuck.5.prism --model-input-type prism --property-input-files pnueli-zuck.props --property-input-names live --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6
Execution
Walltime:14.47735333442688s
Return code:0
Relative Error:0.0
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property live
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 28393 28393
build-model-states-explored 65721 37328
build-model-states-explored 101585 35864
build-model-states-explored 140077 38492
build-model-states-explored 177925 37848
build-model-states-explored 211323 33398
build-model-states-explored 249431 38108
build-model-states-explored 287378 37947
build-model-states-explored 325169 37790
build-model-states-explored 361947 36779
build-model-states-explored 389606 27658
build-model-done 397435 11
iterating
iterating-done 90 0
model-checking-done 13
command-check-result-is 1.0 live